COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDPAR NLSEQ ε SEQ
C00003 00003	AXIOM SETSEQ:
C00005 00004	AXIOM THEOREM:
C00006 ENDMK
C⊗;
DECLARE INDPAR NLSEQ ε SEQ;
DECLARE OPCONST cons(*,SEQ) = SEQ;
DECLARE OPCONST MKSET(SEQ) = SET;
DECLARE INDPAR NLSET ε SET;
DECLARE OPCONST car(SEQ) = *;
DECLARE OPCONST cdr(SEQ) = SEQ;
DECLARE INDVAR u v u1 v1 ε SEQ;
DECLARE INDVAR w w1 w2 z z1 z2 ε SET;
DECLARE INDVAR ww ww1 ww2 zz zz1 zz2 ε SETSET;
DECLARE INDVAR x X x1 x2 y y1 y2 Y X1 X2 Y1 Y2;
MG SET ≥{SETSET};
DECLARE OPCONST uni(SETSET) = SET;
DECLARE OPCONST un(SET,SET) = SET;
DECLARE OPCONST II(SET) = SETSET;
DECLARE PREDPAR A 2;
AXIOM SETSEQ:
	∀x u.(x ε MKSET(u) ≡ ¬(u=NLSEQ) ∧ (x = car(u) ∨ x ε MKSET(cdr(u))));
;

AXIOM CONS:
	∀x u.(¬(cons(x,u) = NLSEQ)),
	∀x u.(car(cons(x,u)) = x),
	∀x u.(cdr(cons(x,u)) = u),
	∀u.(¬u=NLSEQ ⊃ u = cons(car(u),cdr(u)));
;

AXIOM EXTENS:
	∀w1 w2.((∀x.(x ε w1 ≡ x ε w2)) ⊃ w1 = w2);
;

AXIOM NULLSE:
	NLSET = MKSET(NLSEQ);
;

AXIOM UNION:
	∀ww x.(x ε uni(ww) ≡ ∃w.(x ε w ∧ w ε ww)),
	∀ w z.(un(w,z) = uni(II(MKSET(cons(w,cons(z,NLSEQ))))));
;

AXIOM SETSET:
	∀w.(∀x.(x ε w ⊃ SET(x)) ⊃ SETSET(w)),
	∀w.(SETSET(w) ⊃ II(w) = w);
;

AXIOM REPLACEMENT:
	∀x.(∃y.A(x,y)∧∀y1 y2.(A(x,y1)∧A(x,y2) ⊃ y1=y2)) ⊃
∀u ∃v .(∀y.(yεv ≡ ∃x.(xεu ∧ A(x,y))));
;
AXIOM THEOREM:
	∀x.(¬(xεNLSET));
;